Nuprl Lemma : bimplies_weakening
12,41
postcript
pdf
u
,
v
:
. (
u
=
v
)
(
(
u
v
))
latex
ProofTree
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
True
,
tt
,
ff
,
if
b
then
t
else
f
fi
,
b
,
p
q
,
p
q
,
b
,
Unit
,
,
A
,
False
,
Lemmas
bool
wf
,
btrue
neq
bfalse
origin
u, v:
. (u = v) 
(
(u 
v))
u, v:. (u = v) ((u v))
T Qx:A. B(x)
b
q qbA